Fix declaration guard injection in SMT translator by subsetpark · Pull Request #59 · subsetpark/pantagruel

subsetpark · 2026-02-23T14:49:46Z

Summary

Bug 1: Guards on declarations (e.g., value t: Thing, active? t => Nat0) were injected into postconditions, making user-written frame conditions vacuous for unguarded elements and producing spurious "not preserved" warnings. Fixed by adding an inject_guards config flag and disabling it for postcondition translation sites.
Bug 2: Primed applications (value' t in post-state invariants) were skipped by collect_body_guards, so post-state invariants lost their guard antecedents while pre-state copies kept them. Fixed by handling EApp(EPrimed name, args) and bare EPrimed name cases, collecting guards in primed form via prime_expr ~bound.
Adds 3 new tests and a regression sample file (samples/smt-examples/guarded-frame.pant)

Test plan

dune build compiles without errors
dune test — all 106 SMT tests pass (3 new)
pant --check /tmp/guard-test.pant — all OK, no spurious WARN
pant --check samples/smt-examples/guarded-frame.pant — all OK
pant --check fgp-buy.pant — regression passes (no declaration guards in this spec)
SMT dump verified: no guard in frame antecedent, performedp in pre-state invariant, performedp_prime in post-state invariant

🤖 Generated with Claude Code

Summary by CodeRabbit

New Features
- Added guard injection configuration option for SMT-based verification, enabling controlled application of declaration guards during translation.
Tests
- Added regression test suite for guarded declarations and state-transition verification scenarios.

Guards on declarations (e.g., `value t: Thing, active? t => Nat0`) were causing spurious "not preserved" warnings due to two bugs: 1. Guards were injected into postconditions, making user-written frame conditions vacuous for unguarded elements. Postconditions define the transition relation and should be asserted as-is. Fixed by adding an `inject_guards` flag to config and disabling it for postcondition translation sites. 2. Primed applications (e.g., `value' t` in post-state invariants) were skipped by `collect_body_guards`, so post-state invariant copies lost their guards while pre-state copies kept them. Fixed by handling `EApp(EPrimed name, args)` and bare `EPrimed name` cases, collecting guards in primed form via `prime_expr ~bound`. Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

coderabbitai · 2026-02-23T14:50:09Z

No actionable comments were generated in the recent review. 🎉

ℹ️ Recent review info

Configuration used: defaults

Review profile: CHILL

Plan: Pro

📥 Commits

Reviewing files that changed from the base of the PR and between 75ec544 and 8cdc2f9.

📒 Files selected for processing (4)

bin/main.ml
lib/smt.ml
samples/smt-examples/guarded-frame.pant
test/test_smt.ml

📝 Walkthrough

Walkthrough

A new inject_guards boolean configuration field is introduced to the SMT module to conditionally control whether guards from guarded function applications are injected during SMT translation. The field is threaded through configuration initialization, translation functions, and guard collection logic.

Changes

Cohort / File(s)	Summary
Configuration Setup `bin/main.ml`, `test/test_smt.ml`	Initialize the new `inject_guards` field in SMT config construction; update test configurations to set the flag (defaulting to true); add new test cases exercising guard injection behavior.
SMT Translation Implementation `lib/smt.ml`	Add `inject_guards` field to the config type; conditionally inject guards in `translate_proposition` and related pathways based on the flag; implement guard collection utilities (`prime_expr`, `prime_guards`) for handling primed names and bound variables; update postcondition handling to disable guard injection where appropriate.
Regression Test Sample `samples/smt-examples/guarded-frame.pant`	New sample file demonstrating guarded declarations with post-state invariant checks, ensuring guards are correctly primed and excluded from postconditions.

Estimated code review effort

🎯 3 (Moderate) | ⏱️ ~25 minutes

Poem

🐰 A guard injection quest, the SMT runtime grew—
With conditionals and priming, the logic shines so true!
Frames and frames now guarded, post-states dance with care,
Logic bounds in config—let's inject with flair! ✨

🚥 Pre-merge checks | ✅ 3

✅ Passed checks (3 passed)

Check name	Status	Explanation
Description Check	✅ Passed	Check skipped - CodeRabbit’s high-level summary is enabled.
Title check	✅ Passed	The title accurately summarizes the main change: fixing declaration guard injection in the SMT translator, which is reflected in the core logic changes across lib/smt.ml, bin/main.ml, and supporting tests.
Docstring Coverage	✅ Passed	No functions found in the changed files to evaluate docstring coverage. Skipping docstring coverage check.

_{✏️ Tip: You can configure your own custom pre-merge checks in the settings.}

✨ Finishing Touches

🧪 Generate unit tests (beta)

Create PR with unit tests
Post copyable unit tests in a comment
Commit unit tests in branch zax--bugfix-guard-injection

_{Comment @coderabbitai help to get the list of available commands and usage tips.}

greptile-apps · 2026-02-23T14:53:03Z

Greptile Summary

This PR fixes two critical bugs in SMT translation of declaration guards. The fix prevents spurious invariant preservation warnings that occur when guards on declarations (e.g., value t: Thing, active? t => Nat0) are incorrectly injected into postconditions.

Key changes:

Added inject_guards config flag to control when declaration guards are injected as antecedents
Disabled guard injection in postconditions (which define the transition relation) to prevent vacuous frame conditions
Enhanced collect_body_guards to handle primed applications (value' t) and bare primed names (EPrimed name)
Moved prime_expr function before collect_body_guards so primed guards can be correctly generated
Updated postcondition translation in all three query generation sites (contradiction, invariant preservation, k-step BMC)

Bug fixes:

Guards on declarations were being injected into postconditions, making user-written frame conditions vacuous for unguarded elements
Primed applications in post-state invariants lost their guard antecedents because collect_body_guards wasn't handling EPrimed cases

Testing:

Added 3 new unit tests covering primed guard collection, inject_guards=false behavior, and end-to-end validation
New regression sample file demonstrates both bugs are fixed
All 106 SMT tests pass

Confidence Score: 5/5

This PR is safe to merge with minimal risk
The fix is well-designed with clear separation of concerns (config flag), comprehensive test coverage (3 new unit tests + regression sample), and follows the existing codebase patterns. All tests pass and the implementation correctly addresses both identified bugs.
No files require special attention

Important Files Changed

Filename	Overview
bin/main.ml	Added `inject_guards: true` to SMT config initialization - straightforward change
lib/smt.ml	Core fix: Added `inject_guards` config flag, moved `prime_expr` before `collect_body_guards`, enhanced guard collection for primed applications, disabled guard injection in postconditions
test/test_smt.ml	Added 3 new test cases for the guard injection fix and updated existing test configs with `inject_guards: true` field
samples/smt-examples/guarded-frame.pant	New regression test file for declaration guard injection - demonstrates the two fixed bugs

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[SMT Config] -->|inject_guards flag| B{Translation Site}
    B -->|Invariant/Frame| C[inject_guards = true]
    B -->|Postcondition| D[inject_guards = false]
    C --> E[collect_body_guards]
    D --> F[translate_proposition]
    E -->|EApp EPrimed name, args| G[Handle Primed Apps]
    E -->|EPrimed name| H[Handle Bare Primed]
    G --> I[prime_expr with ~bound]
    H --> I
    I --> J[Primed Guard: active?' t]
    F --> K[No Guard Injection]
    C --> L[Guard Antecedent Added]
    K --> M[Postcondition Defines Transition]
    L --> N[Invariant Checking in Next State]

_{Last reviewed commit: 8cdc2f9}

subsetpark merged commit 2a9252e into master Feb 23, 2026
3 checks passed

subsetpark deleted the zax--bugfix-guard-injection branch February 23, 2026 15:06

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Fix declaration guard injection in SMT translator#59

Fix declaration guard injection in SMT translator#59
subsetpark merged 1 commit intomasterfrom
zax--bugfix-guard-injection

subsetpark commented Feb 23, 2026 •

edited by coderabbitai bot

Loading

Uh oh!

coderabbitai bot commented Feb 23, 2026 •

edited

Loading

Walkthrough

Changes

Estimated code review effort

Poem

Uh oh!

greptile-apps bot commented Feb 23, 2026

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

Conversation

subsetpark commented Feb 23, 2026 • edited by coderabbitai bot Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Summary

Test plan

Summary by CodeRabbit

Uh oh!

coderabbitai bot commented Feb 23, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Walkthrough

Changes

Estimated code review effort

Poem

Uh oh!

greptile-apps bot commented Feb 23, 2026

Greptile Summary

Confidence Score: 5/5

Important Files Changed

Flowchart

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

1 participant

subsetpark commented Feb 23, 2026 •

edited by coderabbitai bot

Loading

coderabbitai bot commented Feb 23, 2026 •

edited

Loading